{
 "metadata": {
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  },
  "orig_nbformat": 2,
  "kernelspec": {
   "name": "python3",
   "display_name": "Python 3.7.3 64-bit ('ml2': pyenv)"
  },
  "interpreter": {
   "hash": "8caa4319d59a734f94e739df6b594acde678ec5f2e3eb7152d087fc4a1992669"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2,
 "cells": [
  {
   "cell_type": "markdown",
   "source": [
    "# Strix"
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "source": [
    "from ml2.ltl import LTLSpec\n",
    "from ml2.tools.strix import Strix"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "source": [
    "strix = Strix()"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:ml2.tools.containerized_grpc_service:Pulling Docker image ghcr.io/reactive-systems/ml2/strix-grpc-server:latest\n",
      "INFO:ml2.tools.containerized_grpc_service:Strix container dreamy_keldysh on port 50051 is running\n",
      "INFO:ml2.tools.containerized_grpc_service:Successfully connected to Strix gRPC server running in container dreamy_keldysh on port 50051\n"
     ]
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "source": [
    "spec_dict = {\n",
    "    \"guarantees\": [\n",
    "        \"(G ((((! (g_0)) && (! (g_1))) && ((! (g_2)) || (! (g_3)))) || ((((! (g_0)) || (! (g_1))) && (! (g_2))) && (! (g_3)))))\",\n",
    "        \"(G ((r_0) -> (F (g_0))))\",\n",
    "        \"(G ((r_1) -> (F (g_1))))\",\n",
    "        \"(G ((r_2) -> (F (g_2))))\",\n",
    "        \"(G ((r_3) -> (F (g_3))))\"\n",
    "      ],\n",
    "      \"inputs\": [\n",
    "        \"r_0\",\n",
    "        \"r_1\",\n",
    "        \"r_2\",\n",
    "        \"r_3\",\n",
    "        \"r_4\"\n",
    "      ],\n",
    "      \"outputs\": [\n",
    "        \"g_0\",\n",
    "        \"g_1\",\n",
    "        \"g_2\",\n",
    "        \"g_3\",\n",
    "        \"g_4\"\n",
    "      ],\n",
    "}"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "source": [
    "spec = LTLSpec.from_dict(spec_dict)"
   ],
   "outputs": [],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "source": [
    "strix.synthesize(spec)"
   ],
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "(<LTLSynStatus.REALIZABLE: 'realizable'>,\n",
       " 'aag 12 5 2 5 5\\n2\\n4\\n6\\n8\\n10\\n12 13\\n14 24\\n16\\n18\\n20\\n22\\n0\\n16 15 13\\n18 15 12\\n20 14 13\\n22 14 12\\n24 23 17\\ni0 r_0\\ni1 r_1\\ni2 r_2\\ni3 r_3\\ni4 r_4\\nl0 l0\\nl1 l1\\no0 g_0\\no1 g_1\\no2 g_2\\no3 g_3\\no4 g_4')"
      ]
     },
     "metadata": {},
     "execution_count": 5
    }
   ],
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "source": [
    "del strix"
   ],
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "INFO:ml2.tools.containerized_grpc_service:Stopped and removed container dreamy_keldysh running Strix on port 50051\n"
     ]
    }
   ],
   "metadata": {}
  }
 ]
}